\begin{tabbing}
es{-}pstar{-}q(${\it es}$;$a$,$b$.$p$($a$;$b$);$a$,$b$.$q$($a$;$b$);$e_{1}$;$e_{2}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$\=$m$:$\mathbb{N}^{+}$\+
\\[0ex]$\exists$\=$f$:int\_seg(0; $m$)$\rightarrow$\{$e$:es{-}E(${\it es}$)$\mid$ es{-}loc(${\it es}$; $e$) = es{-}loc(${\it es}$; $e_{1}$) $\in$ Id\} \+
\\[0ex]((($f$(0) = $e_{1}$ $\in$ es{-}E(${\it es}$)) $\wedge$ es{-}le(${\it es}$; ($f$($m$ {-} 1)); $e_{2}$))
\\[0ex]$\wedge$ \=(($\forall$$i$:int\_seg(0; ($m$ {-} 1)). es{-}locl(${\it es}$; ($f$($i$)); ($f$($i$ + 1))))\+
\\[0ex]$\wedge$ ($\forall$$i$:int\_seg(0; ($m$ {-} 1)). $p$($f$($i$);es{-}pred(${\it es}$; ($f$($i$ + 1))))))
\-\\[0ex]$\wedge$ $q$($f$($m$ {-} 1);$e_{2}$))
\-\-
\end{tabbing}